(0) Obligation:
Clauses:
f(0, Y, Z) :- ','(!, eq(Z, 0)).
f(X, Y, Z) :- ','(p(X, P), ','(f(P, Y, U), f(U, Y, Z))).
p(0, 0).
p(s(X), X).
eq(X, X).
Query: f(g,a,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
fB(s(X1), X2, X3) :- fB(X1, X2, X4).
fB(s(X1), X2, X3) :- ','(fcB(X1, X2, X4), fB(X4, X2, X3)).
fA(s(X1), X2, X3) :- fB(X1, X2, X4).
fA(s(X1), X2, X3) :- ','(fcB(X1, X2, X4), fA(X4, X2, X3)).
Clauses:
fcA(0, X1, 0).
fcA(s(X1), X2, X3) :- ','(fcB(X1, X2, X4), fcA(X4, X2, X3)).
fcB(0, X1, 0).
fcB(s(X1), X2, X3) :- ','(fcB(X1, X2, X4), fcB(X4, X2, X3)).
Afs:
fA(x1, x2, x3) = fA(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
fA_in: (b,f,f)
fB_in: (b,f,f)
fcB_in: (b,f,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
FA_IN_GAA(s(X1), X2, X3) → U4_GAA(X1, X2, X3, fB_in_gaa(X1, X2, X4))
FA_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
FB_IN_GAA(s(X1), X2, X3) → U1_GAA(X1, X2, X3, fB_in_gaa(X1, X2, X4))
FB_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
FB_IN_GAA(s(X1), X2, X3) → U2_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U2_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U3_GAA(X1, X2, X3, fB_in_gaa(X4, X2, X3))
U2_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FB_IN_GAA(X4, X2, X3)
FA_IN_GAA(s(X1), X2, X3) → U5_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U6_GAA(X1, X2, X3, fA_in_gaa(X4, X2, X3))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FA_IN_GAA(X4, X2, X3)
The TRS R consists of the following rules:
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U10_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U10_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U11_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U11_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
fA_in_gaa(
x1,
x2,
x3) =
fA_in_gaa(
x1)
s(
x1) =
s(
x1)
fB_in_gaa(
x1,
x2,
x3) =
fB_in_gaa(
x1)
fcB_in_gaa(
x1,
x2,
x3) =
fcB_in_gaa(
x1)
0 =
0
fcB_out_gaa(
x1,
x2,
x3) =
fcB_out_gaa(
x1,
x3)
U10_gaa(
x1,
x2,
x3,
x4) =
U10_gaa(
x1,
x4)
U11_gaa(
x1,
x2,
x3,
x4,
x5) =
U11_gaa(
x1,
x5)
FA_IN_GAA(
x1,
x2,
x3) =
FA_IN_GAA(
x1)
U4_GAA(
x1,
x2,
x3,
x4) =
U4_GAA(
x1,
x4)
FB_IN_GAA(
x1,
x2,
x3) =
FB_IN_GAA(
x1)
U1_GAA(
x1,
x2,
x3,
x4) =
U1_GAA(
x1,
x4)
U2_GAA(
x1,
x2,
x3,
x4) =
U2_GAA(
x1,
x4)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
U5_GAA(
x1,
x2,
x3,
x4) =
U5_GAA(
x1,
x4)
U6_GAA(
x1,
x2,
x3,
x4) =
U6_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FA_IN_GAA(s(X1), X2, X3) → U4_GAA(X1, X2, X3, fB_in_gaa(X1, X2, X4))
FA_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
FB_IN_GAA(s(X1), X2, X3) → U1_GAA(X1, X2, X3, fB_in_gaa(X1, X2, X4))
FB_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
FB_IN_GAA(s(X1), X2, X3) → U2_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U2_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U3_GAA(X1, X2, X3, fB_in_gaa(X4, X2, X3))
U2_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FB_IN_GAA(X4, X2, X3)
FA_IN_GAA(s(X1), X2, X3) → U5_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U6_GAA(X1, X2, X3, fA_in_gaa(X4, X2, X3))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FA_IN_GAA(X4, X2, X3)
The TRS R consists of the following rules:
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U10_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U10_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U11_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U11_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
fA_in_gaa(
x1,
x2,
x3) =
fA_in_gaa(
x1)
s(
x1) =
s(
x1)
fB_in_gaa(
x1,
x2,
x3) =
fB_in_gaa(
x1)
fcB_in_gaa(
x1,
x2,
x3) =
fcB_in_gaa(
x1)
0 =
0
fcB_out_gaa(
x1,
x2,
x3) =
fcB_out_gaa(
x1,
x3)
U10_gaa(
x1,
x2,
x3,
x4) =
U10_gaa(
x1,
x4)
U11_gaa(
x1,
x2,
x3,
x4,
x5) =
U11_gaa(
x1,
x5)
FA_IN_GAA(
x1,
x2,
x3) =
FA_IN_GAA(
x1)
U4_GAA(
x1,
x2,
x3,
x4) =
U4_GAA(
x1,
x4)
FB_IN_GAA(
x1,
x2,
x3) =
FB_IN_GAA(
x1)
U1_GAA(
x1,
x2,
x3,
x4) =
U1_GAA(
x1,
x4)
U2_GAA(
x1,
x2,
x3,
x4) =
U2_GAA(
x1,
x4)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
U5_GAA(
x1,
x2,
x3,
x4) =
U5_GAA(
x1,
x4)
U6_GAA(
x1,
x2,
x3,
x4) =
U6_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 5 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FB_IN_GAA(s(X1), X2, X3) → U2_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U2_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FB_IN_GAA(X4, X2, X3)
FB_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
The TRS R consists of the following rules:
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U10_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U10_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U11_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U11_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
fcB_in_gaa(
x1,
x2,
x3) =
fcB_in_gaa(
x1)
0 =
0
fcB_out_gaa(
x1,
x2,
x3) =
fcB_out_gaa(
x1,
x3)
U10_gaa(
x1,
x2,
x3,
x4) =
U10_gaa(
x1,
x4)
U11_gaa(
x1,
x2,
x3,
x4,
x5) =
U11_gaa(
x1,
x5)
FB_IN_GAA(
x1,
x2,
x3) =
FB_IN_GAA(
x1)
U2_GAA(
x1,
x2,
x3,
x4) =
U2_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
(8) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FB_IN_GAA(s(X1)) → U2_GAA(X1, fcB_in_gaa(X1))
U2_GAA(X1, fcB_out_gaa(X1, X4)) → FB_IN_GAA(X4)
FB_IN_GAA(s(X1)) → FB_IN_GAA(X1)
The TRS R consists of the following rules:
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U10_gaa(X1, fcB_in_gaa(X1))
U10_gaa(X1, fcB_out_gaa(X1, X4)) → U11_gaa(X1, fcB_in_gaa(X4))
U11_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
The set Q consists of the following terms:
fcB_in_gaa(x0)
U10_gaa(x0, x1)
U11_gaa(x0, x1)
We have to consider all (P,Q,R)-chains.
(10) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
FB_IN_GAA(s(X1)) → U2_GAA(X1, fcB_in_gaa(X1))
FB_IN_GAA(s(X1)) → FB_IN_GAA(X1)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(FB_IN_GAA(x1)) = 2 + 2·x1
POL(U10_gaa(x1, x2)) = 1 + x1 + x2
POL(U11_gaa(x1, x2)) = 1 + 2·x1 + x2
POL(U2_GAA(x1, x2)) = 2 + 2·x1 + 2·x2
POL(fcB_in_gaa(x1)) = x1
POL(fcB_out_gaa(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + 2·x1
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GAA(X1, fcB_out_gaa(X1, X4)) → FB_IN_GAA(X4)
The TRS R consists of the following rules:
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U10_gaa(X1, fcB_in_gaa(X1))
U10_gaa(X1, fcB_out_gaa(X1, X4)) → U11_gaa(X1, fcB_in_gaa(X4))
U11_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
The set Q consists of the following terms:
fcB_in_gaa(x0)
U10_gaa(x0, x1)
U11_gaa(x0, x1)
We have to consider all (P,Q,R)-chains.
(12) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(13) TRUE
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FA_IN_GAA(s(X1), X2, X3) → U5_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FA_IN_GAA(X4, X2, X3)
The TRS R consists of the following rules:
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U10_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U10_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U11_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U11_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
fcB_in_gaa(
x1,
x2,
x3) =
fcB_in_gaa(
x1)
0 =
0
fcB_out_gaa(
x1,
x2,
x3) =
fcB_out_gaa(
x1,
x3)
U10_gaa(
x1,
x2,
x3,
x4) =
U10_gaa(
x1,
x4)
U11_gaa(
x1,
x2,
x3,
x4,
x5) =
U11_gaa(
x1,
x5)
FA_IN_GAA(
x1,
x2,
x3) =
FA_IN_GAA(
x1)
U5_GAA(
x1,
x2,
x3,
x4) =
U5_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FA_IN_GAA(s(X1)) → U5_GAA(X1, fcB_in_gaa(X1))
U5_GAA(X1, fcB_out_gaa(X1, X4)) → FA_IN_GAA(X4)
The TRS R consists of the following rules:
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U10_gaa(X1, fcB_in_gaa(X1))
U10_gaa(X1, fcB_out_gaa(X1, X4)) → U11_gaa(X1, fcB_in_gaa(X4))
U11_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
The set Q consists of the following terms:
fcB_in_gaa(x0)
U10_gaa(x0, x1)
U11_gaa(x0, x1)
We have to consider all (P,Q,R)-chains.
(17) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
FA_IN_GAA(s(X1)) → U5_GAA(X1, fcB_in_gaa(X1))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(FA_IN_GAA(x1)) = 2 + 2·x1
POL(U10_gaa(x1, x2)) = 1 + x1 + x2
POL(U11_gaa(x1, x2)) = 1 + 2·x1 + 2·x2
POL(U5_GAA(x1, x2)) = 2 + x1 + 2·x2
POL(fcB_in_gaa(x1)) = x1
POL(fcB_out_gaa(x1, x2)) = x1 + 2·x2
POL(s(x1)) = 1 + 2·x1
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U5_GAA(X1, fcB_out_gaa(X1, X4)) → FA_IN_GAA(X4)
The TRS R consists of the following rules:
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U10_gaa(X1, fcB_in_gaa(X1))
U10_gaa(X1, fcB_out_gaa(X1, X4)) → U11_gaa(X1, fcB_in_gaa(X4))
U11_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
The set Q consists of the following terms:
fcB_in_gaa(x0)
U10_gaa(x0, x1)
U11_gaa(x0, x1)
We have to consider all (P,Q,R)-chains.
(19) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(20) TRUE